package com.googlecode.kipler.satisfiability.completion.rule.formula;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.FormulaCategory;
import com.googlecode.kipler.container.dl.PBox;
import com.googlecode.kipler.satisfiability.completion.branching.BetaBranchingPoint;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation.BetaFormula;
import com.googlecode.kipler.satisfiability.reasoner.BranchingException;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.Formula;


public class BetaFormulaRule extends CompletionRule {

	private boolean applied;

	private Reasoner reasoner;

	private FormulaCategory category;

	private BetaFormula beta;

	private String ruleName;

	private boolean marking;

	private PBox pBox;

	public BetaFormulaRule(Reasoner reasoner, FormulaCategory category,
			BetaFormula beta, boolean marking, String ruleName) {
		this.reasoner = reasoner;
		this.category = category;
		this.beta = beta;
		this.ruleName = ruleName;
		this.marking = marking;
	}

	public void apply() throws ReasonerException {
		applied = false;
		pBox = getWorld().getPBox();
		for (Iterator<Formula> i = pBox.formulaIterator(category); i.hasNext();) {
			beta.setBeta(i.next());
			if (beta.isValid()) {
				if (!getWorld().contains(beta.getBeta1())
						&& !getWorld().contains(beta.getBeta2())) {
					branchForFormulas(beta);
					applied = true;
					throw new BranchingException();
				}
			}
		}
	}

	private void branchForFormulas(BetaFormula beta)
			throws UnsatisfiableException {
		BetaBranchingPoint bp = new BetaBranchingPoint(marking);
		bp.setWcs(getWcs());
		bp.setWorld(getWorld());
		bp.addFormula(beta.getBeta1());
		bp.addFormula(beta.getBeta2());
		bp.setBranchCause(beta.getBeta());
		reasoner.addBranch(bp);
		getWcs().getData().getLogger().info(
				"WCS " + getWcs().getId() + " " + ruleName + ": Branching for "
						+ beta.getBeta1() + " and " + beta.getBeta2());

	}

	/**
	 * @return Returns the applied.
	 */
	public boolean isApplied() {
		return applied;
	}
}
